Nuprl Definition : ecl-trans-act 0,22

ecl-trans-act(ds;da;A)(n,L)
== L':event-info(ds;da) List, tr:event-info(ds;da).
== L = (L' @ [tr])
== & let k,s,v = tr in (k  ecl-trans-ks(A)) & ecl-trans-a(A)(n,k,s,v,ecl-trans-state(A;L')) 
latex



clarification:

ecl-trans-act(ds;da;A)(n,L)
== L':event-info(ds;da) List, tr:event-info(ds;da).
== L = (L' @ (tr.nil))  event-info(ds;da) List
== & let k,s,v = tr in 
== & (k  ecl-trans-ks(A Knd) & ecl-trans-a(A)(n,k,s,v,ecl-trans-state(A;L')) 
latex


Definitionsx:AB(x), P & Q, event-info(ds;da), as @ bs, let x,y,z = a in t(x;y;z), A & B, (x  l), ecl-trans-ks(v), Knd, b, ecl-trans-a(v), ecl-trans-state(v;L)
FDL editor aliasesecl-trans-act

origin